00050	
00100	≤(x,y) ≡ =(/(x,y),0) ;
00200	≤(/(x,y),x);
00300	≤( /(/(x,z),/(y,z)), /(/(x,y),z) );
00400	≤(0,x);
00600	≤(x,y) ∧ ≤(y,x) ⊃ =(x,y);
00700	≤(x,1) ;;
00800	≤(x,y) ⊃ ≤(/(x,z),/(y,z));
00850	=(/(1,/(1,x)),/(x,/(1,x)));
00900	 =(/(x,x),0); =(/(x,1),0); =(/(0,x),0);
01000	∀(x,y,z)( ≤( x, y) ∧ ≤( y,z) ⊃ ≤( x, z));
01100	∀(x)=(/(x,0),x);∀(x,y,z)(≤(/(x,y),z) ⊃ ≤(/(x,z ),y)); 
01200	∀(x,y,z)(≤(x,y) ⊃ ≤(/(z,y),/(z,x)));;
01250	
01300	
01400	∀(x,y)(=(/(1,x),/(1,y)) ⊃=(/(1,/(x,y)),1));;
01500	
01600	
01700